\begin{tabbing}
R{-}interface($A$;$B$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$l$:IdLnk, ${\it tg}$:Id.\+
\\[0ex]fpf{-}cap(R{-}da($A$;source($l$));KindDeq;rcv($l$,${\it tg}$);Void)
\\[0ex]$\subseteq\rho$ fpf{-}cap(R{-}da($B$;destination($l$));KindDeq;rcv($l$,${\it tg}$);Top)
\-
\end{tabbing}